Fonction 91 de McCarthy

La fonction 91 de McCarthy est une fonction récursive définie par McCarthy dans son étude de propriétés de programmes récursifs, et notamment de leur vérification formelle. Avec la fonction de Takeuchi, elle est un exemple amplement repris dans les manuels de programmation.

Définition

La fonction 91 de McCarthy est une fonction récursive définie pour $n\in \mathbb {N}$ par

$f(n)={\begin{cases}n-10&{\rm {\ si\ }}n>100\\f(f(n+11))&{\rm {\ sinon.}}\end{cases}}$

ou, dans la notation de Knuth :

$f(n)=$ si $n>100$ alors $n-10$ sinon $f(f(n+11))$.

On peut démontrer qu'elle est en fait constante et égale à 91 pour $n\leqslant 101$.

Histoire

La fonction 91 a été introduite en 1970 dans des articles de Zohar Manna, Amir Pnueli et John McCarthy, qui sont les prémices de la recherche sur les méthodes formelles de vérification de programmes. La fonction 91 est réellement récursive (avec de multiples appels récursifs imbriqués) par opposition à des fonctions avec récursivité terminale. Cette fonction a été popularisée par le livre de Manna Mathematical Theory of Computation, puis citée en 1978 dans le livre en français de C. Livercy Théorie des programmes. Donald Knuth en a présenté l'historique et des extensions en 1991.

La fonction a été citée maintes fois dans la littérature de recherche, car elle est apparue alors comme un défi pour les méthodes de vérification de programmes.

Exemples d'évaluation

Premier exemple

f(99) = f(f(110)) car 99 ≤ 100
      = f(100)    car 110 > 100
      = f(f(111)) car 100 ≤ 100
      = f(101)    car 111 > 100
      = 91        car 101 > 100

Deuxième exemple

f(87) = f(f(98))
      = f(f(f(109)))
      = f(f(99))
      = f(f(f(110)))
      = f(f(100))
      = f(f(f(111)))
      = f(f(101))
      = f(91)
      = f(f(102))
      = f(92)
      = f(f(103))
      = f(93)
      ... 
      = f(99)
      ...
      = 91

Démonstration

Pour démontrer que $f(n)=91$ pour tout entier $n\leqslant 101$, on considère d'abord le cas $90\leq n\leq 100$ ; on a alors

$f(n)=f(f(n+11))=f(n+1)$

parce que $n+11>100$ ; on a donc

$f(90)=f(91)=\cdots =f(100)=f(101)=91$.

Comme $f(n)=91$ pour les entiers d'un intervalle de 11 valeurs consécutives, on peut utiliser une récurrence pour les valeurs inférieures à 90, et on a $f(n)=f(f(n+11))=f(91)=91$ pour $n\leq 89$ aussi.

Transformation en récursion terminale

On peut considérer la fonction récursive terminale g définie par

$g(n,c)={\begin{cases}n,&{\mbox{si }}c=0\\g(n-10,c-1),&{\mbox{si }}n>100{\mbox{ et }}c\neq 0\\g(n+11,c+1),&{\mbox{si }}n\leq 100{\mbox{ et }}c\neq 0.\end{cases}}$

et on a

$f(n)=g(n,1)$

parce que

$f^{c}(n)=g(n,c)$,

où $f^{c}$ dénote l'application $c$ fois de $f$ (p. ex. $f^{3}(n)=f(f(f(n)))$).

Une variante mutuellement récursive terminale est la définition :

$f(n)=h(n,0)$

avec

$h(n,c)={\begin{cases}h'(n-10,c),&{\mbox{si }}n>100{\mbox{ }}\\h(n+11,c+1),&{\mbox{si }}n\leq 100{\mbox{ }}\end{cases}}$

$h'(n,c)={\begin{cases}n,&{\mbox{si }}c=0{\mbox{ }}\\h(n,c-1),&{\mbox{si }}c\neq 0{\mbox{ }}\end{cases}}$

Une dérivation formelle de la version mutuellement récursive à partir de la version récursive initiale a été donnée par Mitchell Wand, en utilisant les continuations.

Généralisations de Knuth

Donald Knuth, dans son article, considère des généralisations de la fonction, et notamment des itérés $f^{c}$ de la fonction, et illustre en particulier $f^{91}$ par une définition

$f(n)=$ si $n>100$ alors $n-10$ sinon $f^{91}(n+901)$

Il montre que $f(91)=91$ pour cette fonction aussi. Il regarde ensuite la généralisation

$f(n)=$ si $n>a$ alors $n-b$ sinon $f^{c}(n+d)$,

et il montre que la fonction ainsi définie est totale si et seulement si $(c-1)b<d$. Dans ce cas, la fonction vérifie aussi la relation plus simple

$f(n)=$ si $n>a$ alors $n-b$ sinon $f(n+d-(c-1)b)$.

Bibliographie

• [Manna & Pnueli] (en) Zohar Manna et Amir Pnueli, « Formalization of Properties of Functional Programs », Journal of the ACM, vol. 17, n^o 3,‎ juillet 1970, p. 555–569 (DOI 10.1145/321592.321606)
• [Manna & McCarthy] (en) =Zohar Manna et John McCarthy, « Properties of programs and partial function logic », Machine Intelligence, vol. 5,‎ 1970, p. 27-37
• [Manna] Zohar Manna, Mathematical Theory of Computation, New-York, McGraw-Hill, 1974 — Réimpression en 2003 par Dover Publications.
• [Wand] (en) Mitchell Wand, « Continuation-Based Program Transformation Strategies », Journal of the ACM, vol. 27, n^o 1,‎ janvier 1980, p. 164–180 (DOI 10.1145/322169.322183)
• [Knuth] Donald E. Knuth, « Textbook Examples of Recursion », dans Vladimir Lifschitz (éditeur), Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, 490 p. (ISBN 0124500102, arXiv cs/9301113), p. 207-229
• [Livercy] C. Livercy (préf. Claude Pair), Théorie des programmes : Schémas, preuves, sémantique, Paris, Dunod, 1978, xii+328 (ISBN 2-04-010516-6, SUDOC 000231142, lire en ligne), p. 23 — Livercy est le nom collectif de Jean-Pierre Finance, Monique Grandbastien, Pierre Lescanne, Pierre Marchand, Roger Mohr, Alain Quéré, Jean-Luc Rémy

Voir aussi

• Fonction de Takeuchi
• Fonction d'Ackermann